The Logic of Provability; Chapter 7
On GL
Def
$ Aがletterlessであるとは$ \emptyset = \mathrm{Atm}(A)のことを指す.
すなわち,$ A ::= \bot \mid A \to A \mid \Box A.命題記号を含まない.
$ Aがletterlessのとき$ Aが正規形であるとは$ Aが$ \Box^i \botの論理結合であることを指す.
すなわち,$ \Box\bot \land \bot, \Box\Box \bot \to \lnot\Box\bot, \botとかのことを指す
Memo
以下$ \vdashは$ \vdash_\mathbf{GL}のことを表すとする.
$ Aがletterlessのとき,正規なletterless論理式$ A_Nが存在して$ \vdash A \leftrightarrow A_N
Memo
命題記号を含まないから文$ \sigmaの選択が意味を成さない.
以下は適当な実現を$ \cdot^*とする,$ A^*
$ Tは$ \bf PAの適当な拡張理論とする.
$ Tの文で$ \sigma ::= \bot \mid \sigma \to \sigma \mid \mathrm{Pr}_T(\ulcorner \sigma \urcorner)に閉じたものをconstatnt sentenceということにする. $ \sigmaがconstatnt sentenceのとき,letterlessな様相論理式$ Aで$ \sigma \equiv A^*となるものが存在する.
Lem1より$ Aは更に正規形$ A_Nに変形できる.
ところで,$ (\Box^i\bot)^* \equiv \mathrm{Pr}(\ulcorner \cdots \mathrm{Pr}_T(\ulcorner \bot \urcorner) \cdots \urcorner)だが,$ \mathrm{Pr}(\ulcorner \cdots \mathrm{Pr}_T(\ulcorner \bot \urcorner) \cdots \urcorner)の真理値は$ \botと同じ.
よって,$ A_Nの$ \Boxを全て削除した命題論理の論理式と真理値と$ \sigmaの真理値は一致する.
命題論理の真理値は明らかに決定可能/計算可能だから,$ \sigmaがconstatnt sentenceであれば$ \sigmaの真理値は決定可能である.
$ \sigmaが証明可能かは$ \sigma \equiv A^*となる$ Aを見つけて$ \Box Aの真理値を決定すれば良い.
Def: ランク
$ \lang W,\prec \rangは有限推移非反射的フレームとする.
$ w_0 \succ w_1 \succ \cdots \succ w_nとなる$ w_0,\dots,w_n \in Wについて
推移律より$ i < jで$ w_i \succ w_j
非反射的なので$ w_i \neq w_j
任意の$ wに対し,$ w_0 \succ w_1 \succ \cdots \succ w_nに出来る最大の$ n \le |W|が存在する
この$ nのことを$ wのランクという.$ \rho_{\lang W,\prec \rang}(w)と表す.
$ \lang W,\prec \rangは省略する.
どこにも繋がらない場合は$ \rho(w) = 0とする.
Lem 2
$ \rho(w) > iなら,ある$ xに対して$ x \prec wで$ \rho(x) = i
proof
$ \rho(w) = n > iとしたとき$ w = w_n \prec \cdots \prec w_1 \prec w_0
このとき$ x = w_iとする.
推移律より$ w_n \prec x
$ \rho(x) = iであることを示す.$ \rho(x) \ge iであることは明らかなので$ \rho(x) \not> iであることを示す.
背理法で$ \rho(x) = j > iとする.このとき$ x = x_j \prec \cdots \prec x_1 \prec x_0
$ w_i = w_jとして接続する.
$ w = w_n \prec \cdots \prec w_{i+1} \prec w_i = x_j \prec \cdots \prec x_i \prec x_0
このとき$ \rho(w) = n-i+j > nとなっておかしい.
Def: トレース
$ Aをletterlessとする.次のように定まる自然数の集合$ \llbracket A \rrbracketを$ Aのトレースという.
$ \llbracket \bot \rrbracket = \empty
$ \llbracket B \to C \rrbracket = (\N - \llbracket B \rrbracket) \cup \llbracket C \rrbracket
$ \llbracket \Box B \rrbracket = \{n \mid \forall_{i < n}. i \in \llbracket B \rrbracket\}
example
$ \llbracket \Box\bot \rrbracket = \{0\}
$ \llbracket \Box\Box\bot \rrbracket = \{ n \mid \forall_{i<n}.i \in \{0\} \} = \{0,1\}
$ \llbracket \Box\Box\bot \to \Box\bot \rrbracket = \N - \{0,1\} \cup \{ 0\} = \N - \{1\}
example
$ \llbracket \lnot B \rrbracket = \llbracket B \to \bot \rrbracket = \N - \llbracket B \rrbracket
memo
Lem 3
任意のletterlessな$ Aのトレース$ \llbracket A \rrbracketは有限か補有限である.
proof
Lem 4
有限推移非反射的なモデル$ \mathcal{M}とその$ wとし,$ Aはletterlessとする.
$ w \Vdash_\mathcal{M} A \iff \rho(w) \in \llbracket A \rrbracket
proof
$ A \equiv \botなら$ w \nVdash \botだから明らか.
$ A \equiv B \to Cのとき
$ w \Vdash B \to C
$ \iff$ w \nVdash Bまたは$ w \Vdash C
$ \iff$ \rho(w) \notin \llbracket B \rrbracketまたは$ \rho(w) \in \llbracket C \rrbracket
$ \iff$ \rho(w) \in (\N - \llbracket B \rrbracket) \cup \llbracket C \rrbracket
$ \iff \rho(w) \in \llbracket B \to C \rrbracket
$ A \equiv \Box Bのとき
対偶を示す.
$ w \nVdash \Box B$ \implies$ w \prec xで$ x \nVdash Bな$ xが存在
帰納法の仮定より$ \rho(x) \notin \llbracket B \rrbracket
$ w \prec xだから$ \rho(x) + 1 \le \rho(w)すなわち$ \rho(x) <\rho(w)
よって$ \rho(w) \notin \llbracket \Box B \rrbracket
$ \rho(w) \notin \llbracket \Box B \rrbracket$ \impliesある$ i < \rho(w)で$ \rho(w) \notin \llbracket B \rrbracket
Lem2より$ w \prec xで$ \rho(x) = iとなる$ xが存在する
帰納法の仮定より$ x \nVdash Bだから,$ w \nVdash \Box B.
Lem 5
$ Aがletterlessなら$ \vdash_\mathbf{GL} A \iff \llbracket A \rrbracket = \N
memo
$ \bf GLの完全性定理は仮定する.$ \vdash_\mathbf{GL} A \iff \mathcal{M} \vDash A
$ \mathcal{M}は有限推移非反射的.
proof
$ \vdash_\mathbf{GL} Aのとき
以下を満たす有限推移非反射的モデル$ \mathcal{M} = \lang W,\prec,V \rangが存在する
任意の$ nについて,ある$ wで$ \rho(w) = n
$ w \Vdash_\mathcal{M} A
Lem 2より$ n = \rho(w) \in \llbracket A \rrbracket.
$ nは任意だから$ \llbracket A \rrbracket = \N
対偶を示す.$ \nvdash_\mathbf{GL} A \implies \llbracket A \rrbracket \neq \N
$ \nvdash_\mathbf{GL} Aだとすると適当な$ \mathcal{M},wが存在して$ w \nVdash_\mathcal{M} A
Lem4より$ \rho(w) \notin \llbracket A \rrbracket
Prop 6
$ \llbracket B \rrbracket \sube \llbracket C \rrbracket \iff \vdash_\mathbf{GL} B \to C
$ \llbracket B \rrbracket = \llbracket C \rrbracket \iff \vdash_\mathbf{GL} B \leftrightarrow C
Lem 7
任意の$ nに対して$ \llbracket \Box^n\bot \rrbracket =\{ m \mid m < n\}
proof
$ \llbracket \Box^0\bot \rrbracket = \llbracket \bot \rrbracket = \emptyset = \{m \mid m < 0 \}
$ \llbracket \Box^k\bot \rrbracket = \{m \mid m < k \}とすると$ \llbracket \Box^{k+1}\bot \rrbracket = \{n \mid \forall_{i < n}. i \in \llbracket \Box^k\bot \rrbracket\} = \{ m \mid m < k + 1 \}
Lem 8
$ \llbracket \lnot(\Box^{n+1} \bot \to \Box^n\bot) \rrbracket = \{n\}
proof
$ \llbracket \lnot(\Box^{n+1} \bot \to \Box^n\bot) \rrbracket
$ = \N - \llbracket \Box^{n+1} \bot \to \Box^n\bot \rrbracket
$ = \N - ((\N - \llbracket \Box^{n+1}\bot \rrbracket) \cup \llbracket \Box^n\bot \rrbracket)
$ = \N - (\{ m \mid n+1 \lt m \} \cup \{m \mid m < n \})
$ = \{n\}
Lem 9
$ \llbracket A \rrbracketは有限とする.$ B = \bigvee \{ \lnot(\Box^{n+1}\bot \to \Box^n\bot) \mid n \in \llbracket A \rrbracket \}.
$ \vdash_\mathbf{GL} A \leftrightarrow B
proof
Lem 10
$ \llbracket A \rrbracketは補有限とする.$ B = \bigwedge \{ \lnot(\Box^{n+1}\bot \to \Box^n\bot) \mid n \in \llbracket A \rrbracket \}.
$ \vdash_\mathbf{GL} A \leftrightarrow B
proof: Lem9と同様に
Memo
Lem3とLem9/10よりThm1(正規化)が証明される.